Search for: All records

We present SERBERUS, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL, and/or PSF speculation primitives) on existing hardware. SERBERUS is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives—instructions that can transiently assign a secret value to a publicly-typed register. We evaluate SERBERUS on cryptographic primitives in the OPENSSL, LIBSODIUM, and HACL* libraries. SERBERUS introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure. 

Modern hardware complexity makes it challenging to determine if a given microarchitecture adheres to a particular memory consistency model (MCM). This observation inspired the Check tools, which formally check that a specific microarchitecture correctly implements an MCM with respect to a suite of litmus test pro-grams. Unfortunately, despite their effectiveness and efficiency, theCheck tools must be supplied a microarchitecture in the guise of a manually constructed axiomatic specification, called a 𝜇spec model. To facilitate MCM verification—and enable the Check tools to consume processor RTL directly—we introduce a methodology and associated tool, rtl2𝜇spec, for automatically synthesizing 𝜇spec models from processor designs written in Verilog or SystemVerilog, with the help of modest user-provided design metadata. As a case study, we use rtl2𝜇spec to facilitate the Check-based verification of the four-core RISC-V V-scale (multi-V-scale) processor’s MCM implementation. We show that rtl2𝜇spec can synthesize a complete, and proven correct by construction, 𝜇spec model from the SystemVerilog design of the multi-V-scale processor in 6.84 minutes. Subsequent Check-based MCM verification of the synthesized 𝜇spec model takes less than one second per litmus test.